
; Copyright (c) 2015 Microsoft Corporation


(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)

(simplify (< 1 2))
(simplify (< 3 2))
(simplify (< 2 2))
(simplify (<= 1 2))
(simplify (<= 2 2))
(simplify (<= 3 2))
(simplify (> 1 2))
(simplify (> 2 2))
(simplify (> 3 2))
(simplify (>= 1 2))
(simplify (>= 2 2))
(simplify (>= 3 2))
(simplify (< a (+ b 1)))
(simplify (< a (+ b 1))
                 :arith-lhs true)
(simplify (< a (+ b a 1))
                 :arith-lhs true)
(simplify (< a (+ b a a 1))
                 :arith-lhs true)
(simplify (< a (+ b a a 1)))
(simplify (> a (+ b 1))
                 :arith-lhs true)
(simplify (> (* 3 a) (+ b a 1))
                 :arith-lhs true)
(simplify (>= (* 3 a) (+ b a 1))
                 :arith-lhs true)
(simplify (>= (* 3 a) (+ b a 1)))

(simplify (>= (+ (* 3 a) (* 2 b) 4) (+ (* 4 b) a 1 c d)))
(simplify (>= (+ (* 3 a) (* 2 b) 4) (+ (* 4 b) a 1 c d))
                 :arith-lhs true)
(simplify (<= (+ (* 3 a) (* 2 b) 4) (+ (* 4 b) a 1 c d)))
(simplify (<= (+ (* 3 a) (* 2 b) 4) (+ (* 4 b) a 1 c d))
                 :arith-lhs true)
(simplify (<= (+ (* 3 a) (* 2 b) 4) (+ (* 4 b) a 10 c d)))
